T:Type, L:T List, a:T, P:(T).
index-of-first x in a.L.P(x)
~
if P(a) 1 ; 0<index-of-first x in L.P(x) index-of-first x in L.P(x)+1 else 0 fi 

latex

Definitions	b, b, Unit, P  Q, P  Q, hd(l), i<j, ij, ij, , l[i], x(s), t  T, , x:A. B(x), ||as||, {i..j}, Prop, search(k;P), if b t else f fi, {T}, P  Q, False, A, P & Q, AB, i  j < k, True, T, SQType(T), index-of-first x in L.P(x)
Lemmas	int seg wf, length wf1, bool wf, search succ, select wf, length cons, non neg length, search wf, select cons tl, squash wf, le wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, assert of lt int, true wf, bnot of lt int, assert of le int, lt int wf, le int wf, int seg properties